(*  Title:      Restricted_Measure_Space.thy
    Author:     Mnacho Echenim, Univ. Grenoble Alpes
*)

section ‹Generated subalgebras›

text ‹This section contains definitions and properties related to generated subalgebras.›

theory Generated_Subalgebra imports "HOL-Probability.Probability"

begin



definition gen_subalgebra where
"gen_subalgebra M G = sigma (space M) G"


lemma gen_subalgebra_space:
  shows "space (gen_subalgebra M G) = space M"
by (simp add: gen_subalgebra_def space_measure_of_conv)


lemma gen_subalgebra_sets:
  assumes "G ⊆ sets M"
  and "A ∈ G"
  shows "A ∈ sets (gen_subalgebra M G)"
by (metis assms gen_subalgebra_def sets.space_closed sets_measure_of sigma_sets.Basic subset_trans)


lemma gen_subalgebra_sig_sets:
  assumes "G ⊆ Pow (space M)"
  shows "sets (gen_subalgebra M G) = sigma_sets (space M) G" unfolding gen_subalgebra_def
by (metis assms gen_subalgebra_def sets_measure_of)

lemma  gen_subalgebra_sigma_sets:
  assumes "G ⊆ sets M"
  and "sigma_algebra (space M) G"
  shows "sets (gen_subalgebra M G) = G"
using assms by (simp add: gen_subalgebra_def sigma_algebra.sets_measure_of_eq)


lemma gen_subalgebra_is_subalgebra:
  assumes sub: "G ⊆ sets M"
  and sigal:"sigma_algebra (space M) G"
  shows "subalgebra M (gen_subalgebra M G)" (is "subalgebra M ?N")
unfolding subalgebra_def
proof (intro conjI)
  show "space ?N = space M" using space_measure_of_conv[of "(space M)"]  unfolding gen_subalgebra_def by simp
  have geqn: "G = sets ?N" using assms by (simp add:gen_subalgebra_sigma_sets)
  thus "sets ?N ⊆ sets M" using assms by simp
qed


definition  fct_gen_subalgebra :: "'a measure ⇒ 'b measure ⇒ ('a ⇒ 'b) ⇒ 'a measure" where
  "fct_gen_subalgebra M N X = gen_subalgebra M (sigma_sets (space M) {X -` B ∩ (space M) | B. B ∈ sets N})"



lemma fct_gen_subalgebra_sets:
  shows "sets (fct_gen_subalgebra M N X) = sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N}"
unfolding fct_gen_subalgebra_def gen_subalgebra_def
proof -
  have "{X -` B ∩ space M |B. B ∈ sets N} ⊆ Pow (space M)"
    by blast
  then show "sets (sigma (space M) (sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N})) = sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N}"
    by (meson sigma_algebra.sets_measure_of_eq sigma_algebra_sigma_sets)
qed

lemma fct_gen_subalgebra_space:
  shows "space (fct_gen_subalgebra M N X) = space M"
  unfolding fct_gen_subalgebra_def by (simp add: gen_subalgebra_space)

lemma fct_gen_subalgebra_eq_sets:
  assumes "sets M = sets P"
  shows "fct_gen_subalgebra M N X = fct_gen_subalgebra P N X"
proof -
  have "space M = space P" using sets_eq_imp_space_eq assms by auto
  thus ?thesis unfolding fct_gen_subalgebra_def gen_subalgebra_def by simp
qed

lemma fct_gen_subalgebra_sets_mem:
  assumes "B∈ sets N"
  shows "X -` B ∩ (space M) ∈ sets (fct_gen_subalgebra M N X)" unfolding fct_gen_subalgebra_def
proof -
  have f1: "{X -` A ∩ space M |A. A ∈ sets N} ⊆ Pow (space M)"
    by blast
  have "∃A. X -` B ∩ space M = X -` A ∩ space M ∧ A ∈ sets N"
    by (metis assms)
  then show "X -` B ∩ space M ∈ sets (gen_subalgebra M (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets N}))"
    using f1 by (simp add: gen_subalgebra_def sigma_algebra.sets_measure_of_eq sigma_algebra_sigma_sets)
qed

lemma fct_gen_subalgebra_is_subalgebra:
  assumes "X∈ measurable M N"
  shows "subalgebra M (fct_gen_subalgebra M N X)"
unfolding fct_gen_subalgebra_def
proof (rule gen_subalgebra_is_subalgebra)
  show "sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N} ⊆ sets M" (is "?L ⊆ ?R")
  proof (rule sigma_algebra.sigma_sets_subset)
    show "{X -` B ∩ space M |B. B ∈ sets N} ⊆ sets M"
    proof
      fix a
      assume "a ∈ {X -` B ∩ (space M) | B. B ∈ sets N}"
      then obtain B where "B ∈ sets N" and "a = X -` B ∩ (space M)" by auto
      thus "a ∈ sets M" using measurable_sets assms by simp
    qed
    show "sigma_algebra (space M) (sets M)" using measure_space by (auto simp add: measure_space_def)
  qed
  show "sigma_algebra (space M) ?L"
  proof (rule sigma_algebra_sigma_sets)
    let ?preimages = "{X -` B ∩ (space M) | B. B ∈ sets N}"
    show "?preimages ≤ Pow (space M)" using assms by auto
  qed
qed

lemma fct_gen_subalgebra_fct_measurable:
  assumes "X ∈ space M → space N"
  shows "X∈ measurable (fct_gen_subalgebra M N X) N"
unfolding measurable_def
proof ((intro CollectI), (intro conjI))
  have speq: "space M = space (fct_gen_subalgebra M N X)"
      by (simp add: fct_gen_subalgebra_space)
  show "X ∈ space (fct_gen_subalgebra M N X) → space N"
  proof -
    have "X ∈ space M → space N"  using assms by simp
    thus ?thesis using speq by simp
  qed
  show "∀y∈sets N.
       X -` y ∩ space (fct_gen_subalgebra M N X) ∈ sets (fct_gen_subalgebra M N X)"
  using  fct_gen_subalgebra_sets_mem speq by metis
qed




lemma fct_gen_subalgebra_min:
  assumes "subalgebra M P"
  and "f∈ measurable P N"
  shows "subalgebra P (fct_gen_subalgebra M N f)"
unfolding subalgebra_def
proof (intro conjI)
  let ?Mf = "fct_gen_subalgebra M N f"
  show "space ?Mf = space P" using assms
    by (simp add: fct_gen_subalgebra_def gen_subalgebra_space subalgebra_def)
  show inc: "sets ?Mf ⊆ sets P"
  proof -
    have "space M = space P" using assms by (simp add:subalgebra_def)
    have "f∈ measurable M N" using assms using measurable_from_subalg by blast
    have "sigma_algebra (space P) (sets P)" using assms measure_space measure_space_def by auto
    have "∀ A ∈ sets N. f-`A ∩ space P ∈ sets P" using assms by simp
    hence "{f -` A ∩ (space M) | A. A ∈ sets N} ⊆ sets P" using ‹space M = space P› by auto
    hence "sigma_sets (space M) {f -` A ∩ (space M) | A. A ∈ sets N} ⊆ sets P"
      by (simp add: ‹sigma_algebra (space P) (sets P)› ‹space M = space P› sigma_algebra.sigma_sets_subset)
    thus ?thesis using fct_gen_subalgebra_sets ‹f ∈ M →⇩M N› ‹space M = space P› assms(2)
      measurable_sets mem_Collect_eq sets.sigma_sets_subset subsetI by blast
  qed
qed

lemma fct_preimage_sigma_sets:
  assumes "X∈ space M → space N"
  shows "sigma_sets (space M) {X -` B ∩ space M |B. B ∈ sets N} = {X -` B ∩ space M |B. B ∈ sets N}" (is "?L = ?R")
proof
  show "?R⊆ ?L" by blast
  show "?L⊆ ?R"
  proof
    fix A
    assume "A∈ ?L"
    thus "A∈ ?R"
    proof (induct rule:sigma_sets.induct, auto)
      {
        fix B
        assume "B∈ sets N"
        let ?cB = "space N - B"
        have "?cB ∈ sets N" by (simp add: ‹B ∈ sets N› sets.compl_sets)
        have "space M - X -` B ∩ space M = X -` ?cB ∩ space M"
        proof
          show "space M - X -` B ∩ space M ⊆ X -` (space N - B) ∩ space M"
          proof
            fix w
            assume "w ∈ space M - X -` B ∩ space M"
            hence "X w ∈ (space N - B)" using assms by blast
            thus "w∈ X -` (space N - B) ∩ space M" using ‹w ∈ space M - X -` B ∩ space M› by blast
          qed
          show "X -` (space N - B) ∩ space M ⊆ space M - X -` B ∩ space M"
          proof
            fix w
            assume "w∈ X -` (space N - B) ∩ space M"
            thus "w ∈ space M - X -` B ∩ space M" by blast
          qed
        qed
        thus "∃Ba. space M - X -` B ∩ space M = X -` Ba ∩ space M ∧ Ba ∈ sets N" using ‹?cB ∈ sets N› by auto
      }
      {
        fix S::"nat ⇒ 'a set"
        assume "(⋀i. ∃B. S i = X -` B ∩ space M ∧ B ∈ sets N)"
        hence "(∀i. ∃B. S i = X -` B ∩ space M ∧ B ∈ sets N)" by auto
        hence "∃ f. ∀ x. S x = X -`(f x) ∩ space M ∧ (f x) ∈ sets N"
          using choice[of "λi B . S i = X -` B ∩ space M ∧ B ∈ sets N"] by simp
        from this obtain rep where "∀i. S i = X -` (rep i) ∩ space M ∧ (rep i) ∈ sets N" by auto note rProp = this
        let ?uB = "⋃i∈ UNIV. rep i"
        have "?uB ∈ sets N"
          by (simp add: ‹∀i. S i = X -` rep i ∩ space M ∧ rep i ∈ sets N› countable_Un_Int(1))
        have "(⋃x. S x) = X -` ?uB ∩ space M"
        proof
          show "(⋃x. S x) ⊆ X -` (⋃i. rep i) ∩ space M"
          proof
            fix w
            assume "w∈ (⋃x. S x)"
            hence "∃x. w ∈ S x" by auto
            from this obtain x where "w ∈ S x" by auto
            hence "w∈  X -` rep x ∩ space M" using rProp by simp
            hence "w∈ (⋃i. (X -`(rep i)∩ space M))" by blast
            also have "... = X -` (⋃i. rep i) ∩ space M" by auto
            finally show "w ∈ X -` (⋃i. rep i) ∩ space M" .
          qed
          show "X -` (⋃i. rep i) ∩ space M ⊆ (⋃x. S x)"
          proof
            fix w
            assume "w∈ X -` (⋃i. rep i) ∩ space M"
            hence "∃ x. w∈ X -` (rep x) ∩ space M" by auto
            from this obtain x where "w∈ X -` (rep x) ∩ space M" by auto
            hence "w∈ S x" using rProp by simp
            thus "w∈ (⋃x. S x)" by blast
          qed
        qed
        thus "∃B. (⋃x. S x) = X -` B ∩ space M ∧ B ∈ sets N" using ‹?uB ∈ sets N› by auto
      }
    qed
  qed
qed

lemma fct_gen_subalgebra_sigma_sets:
  assumes "X∈ space M → space N"
  shows "sets (fct_gen_subalgebra M N X) = {X -` B ∩ space M |B. B ∈ sets N}"
  by (simp add: assms fct_gen_subalgebra_sets fct_preimage_sigma_sets)


lemma fct_gen_subalgebra_info:
  assumes "f∈ space M → space N"
  and "x∈ space M"
  and "w∈ space M"
  and "f x = f w"
  shows "⋀A. A∈ sets (fct_gen_subalgebra M N f) ⟹ (x∈ A) = (w∈ A)"
proof -
  {fix A
  assume "A ∈ sigma_sets (space M)  {f -` B ∩ (space M) | B. B ∈ sets N}"
  from this have  "(x∈ A) = (w∈ A)"
  proof (induct rule:sigma_sets.induct)
    {
      fix a
      assume "a ∈ {f -` B ∩ space M |B. B ∈ sets N}"
      hence "∃ B∈ sets N. a = f -` B ∩ space M" by auto
      from this obtain B where "B∈ sets N" and "a = f -` B ∩ space M" by blast note bhyps = this
      show "(x∈ a) = (w∈ a)" by (simp add: assms(2) assms(3) assms(4) bhyps(2))
    }
    {
      fix a
      assume "a ∈ sigma_sets (space M) {f -` B ∩ space M |B. B ∈ sets N}"
      and "(x ∈ a) = (w ∈ a)" note xh = this
      show "(x ∈ space M - a) = (w ∈ space M - a)" by (simp add: assms(2) assms(3) xh(2))
    }
    {
      fix a::"nat ⇒ 'a set"
      assume "(⋀i. a i ∈ sigma_sets (space M) {f -` B ∩ space M |B. B ∈ sets N})"
      and "(⋀i. (x ∈ a i) = (w ∈ a i))"
      show "(x ∈ ⋃(a ` UNIV)) = (w ∈ ⋃(a ` UNIV))" by (simp add: ‹⋀i. (x ∈ a i) = (w ∈ a i)›)
    }
    {show "(x∈ {}) = (w∈ {})" by simp}
  qed} note eqsig = this
  fix A
  assume "A∈ sets (fct_gen_subalgebra M N f)"
  hence "A ∈ sigma_sets (space M)  {f -` B ∩ (space M) | B. B ∈ sets N}"
    using assms(1) fct_gen_subalgebra_sets by blast
  thus "(x∈ A) = (w∈ A)" using eqsig by simp
qed

subsection ‹Independence between a random variable and a subalgebra.›

definition (in prob_space) subalgebra_indep_var :: "('a ⇒ real) ⇒ 'a measure ⇒ bool" where
  "subalgebra_indep_var X N ⟷
    X∈ borel_measurable M &
    (subalgebra M N) &
    (indep_set (sigma_sets (space M) { X -` A ∩ space M | A. A ∈ sets borel}) (sets N))"


lemma (in prob_space) indep_set_mono:
  assumes "indep_set A B"
  assumes "A' ⊆ A"
  assumes "B' ⊆ B"
  shows "indep_set A' B'"
by (meson indep_sets2_eq assms subsetCE subset_trans)


lemma (in prob_space) subalgebra_indep_var_indicator:
  fixes X::"'a⇒real"
  assumes "subalgebra_indep_var X N"
  and "X ∈ borel_measurable M"
  and "A ∈ sets N"
  shows "indep_var borel X borel (indicator A)"
proof ((rule indep_var_eq[THEN iffD2]), (intro conjI))
  let ?IA = "(indicator A)::'a⇒ real"
  show bm:"random_variable borel X" by (simp add: assms(2))
  show "random_variable borel ?IA" using assms indep_setD_ev2 unfolding subalgebra_indep_var_def by auto
  show "indep_set (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel})
   (sigma_sets (space M) {?IA -` Aa ∩ space M |Aa. Aa ∈ sets borel})"
  proof (rule indep_set_mono)
    show "sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel} ⊆ sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel}" by simp
    show "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N"
    proof -
      have "sigma_algebra (space M) (sets N)" using assms
        by (metis subalgebra_indep_var_def sets.sigma_algebra_axioms subalgebra_def)
      have "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sigma_sets (space M) (sets N)"
      proof (rule sigma_sets_subseteq)
        show "{?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N"
        proof
          fix x
          assume "x ∈ {?IA -` B ∩ space M |B. B ∈ sets borel}"
          then obtain B where "B ∈ sets borel" and "x = ?IA -` B ∩ space M" by auto
          thus "x ∈ sets N"
            by (metis (no_types, lifting) assms(1) assms(3) borel_measurable_indicator measurable_sets subalgebra_indep_var_def subalgebra_def)
        qed
      qed
      also have "... = sets N"
        by (simp add: ‹sigma_algebra (space M) (sets N)› sigma_algebra.sigma_sets_eq)
      finally show "sigma_sets (space M) {?IA -` B ∩ space M |B. B ∈ sets borel} ⊆ sets N" .
    qed
    show "indep_set (sigma_sets (space M) {X -` A ∩ space M |A. A ∈ sets borel}) (sets N) "
      using assms unfolding subalgebra_indep_var_def by simp
  qed
qed

lemma fct_gen_subalgebra_cong:
  assumes "space M = space P"
  and "sets N = sets Q"
  shows "fct_gen_subalgebra M N X = fct_gen_subalgebra P Q X"
proof -
  have "space M = space P" using assms by simp
  thus ?thesis using assms unfolding fct_gen_subalgebra_def gen_subalgebra_def by simp
qed



end

(*  Title:      Filtration.thy
    Author:     Mnacho Echenim, Univ. Grenoble Alpes
*)

section ‹Filtrations›

text ‹This theory introduces basic notions about filtrations, which permit to define adaptable processes
and predictable processes in the case where the filtration is indexed by natural numbers.›

theory Filtration imports "HOL-Probability.Probability"
begin
subsection ‹Basic definitions›
class linorder_bot = linorder + bot
instantiation nat::linorder_bot
begin
instance proof qed
end


definition filtration :: "'a measure ⇒ ('i::linorder_bot ⇒ 'a measure) ⇒ bool" where
  "filtration M F ⟷
    (∀t. subalgebra M (F t))  ∧
    (∀ s t. s ≤ t ⟶ subalgebra (F t) (F s))"

lemma filtrationI:
  assumes "∀t. subalgebra M (F t)"
  and "∀s t. s ≤ t ⟶ subalgebra (F t) (F s)"
shows "filtration M F" unfolding filtration_def using assms by simp

lemma filtrationE1:
  assumes "filtration M F"
  shows "subalgebra M (F t)" using assms unfolding filtration_def by simp

lemma filtrationE2:
  assumes "filtration M F"
  shows "s≤ t ⟹ subalgebra (F t) (F s)" using assms unfolding filtration_def by simp

locale filtrated_prob_space = prob_space +
  fixes F
  assumes filtration: "filtration M F"

lemma (in filtrated_prob_space) filtration_space:
  assumes "s ≤ t"
  shows "space (F s) = space (F t)" by (metis filtration filtration_def subalgebra_def)

lemma (in filtrated_prob_space) filtration_measurable:
  assumes "f∈ measurable (F t) N"
shows "f∈ measurable M N" unfolding measurable_def
proof
  show "f ∈ space M → space N ∧ (∀y∈sets N. f -` y ∩ space M ∈ sets M)"
  proof (intro conjI ballI)
    have "space (F t) = space M" using assms filtration unfolding filtration_def subalgebra_def by auto
    thus "f∈ space M → space N" using assms unfolding measurable_def by simp
    fix y
    assume "y∈ sets N"
    hence "f -`y∩ space M ∈ sets (F t)" using assms unfolding measurable_def
      using ‹space (F t) = space M› by auto
    thus "f -`y∩ space M ∈ sets M"  using assms filtration unfolding filtration_def subalgebra_def by auto
  qed
qed


lemma (in filtrated_prob_space) increasing_measurable_info:
  assumes "f∈ measurable (F s) N"
  and "s ≤ t"
  shows "f∈ measurable (F t) N"
proof (rule measurableI)
  have inc: "sets (F s) ⊆ sets (F t)"
    using assms(2) filtration by (simp add: filtration_def subalgebra_def)
  have sp: "space (F s) = space (F t)" by (metis filtration filtration_def subalgebra_def)
  thus "⋀x. x ∈ space (F t) ⟹ f x ∈ space N" using assms by (simp add: measurable_space)
  show "⋀A. A ∈ sets N ⟹ f -` A ∩ space (F t) ∈ sets (F t)"
  proof -
    fix A
    assume "A∈ sets N"
    hence "f -` A ∩ space (F s) ∈ sets (F s)" using assms using measurable_sets by blast
    hence "f -` A ∩ space (F s) ∈ sets (F t)" using subsetD[of "F s" "F t"] inc by blast
    thus "f -` A ∩ space (F t) ∈ sets (F t)" using sp by simp
  qed
qed



definition disc_filtr :: "'a measure ⇒ (nat ⇒ 'a measure) ⇒ bool" where
  "disc_filtr M F ⟷
    (∀n. subalgebra M (F n))  ∧
    (∀ n m. n ≤ m ⟶ subalgebra (F m) (F n))"


locale disc_filtr_prob_space = prob_space +
  fixes F
  assumes discrete_filtration: "disc_filtr M F"

lemma (in disc_filtr_prob_space) subalgebra_filtration:
  assumes "subalgebra N M"
  and "filtration M F"
shows "filtration N F"
proof (rule filtrationI)
  show "∀s t. s ≤ t ⟶ subalgebra (F t) (F s)" using assms unfolding filtration_def by simp
  show "∀t. subalgebra N (F t)"
  proof
    fix t
    have "subalgebra M (F t)" using assms unfolding filtration_def by auto
    thus "subalgebra N (F t)" using assms by (metis subalgebra_def subsetCE subsetI)
  qed
qed



sublocale disc_filtr_prob_space ⊆  filtrated_prob_space
proof unfold_locales
  show "filtration M F"
    using  discrete_filtration by (simp add: filtration_def disc_filtr_def)
qed



subsection ‹Stochastic processes›

text  ‹Stochastic processes are collections of measurable functions. Those of a particular interest when
there is a filtration are the adapted stochastic processes.›

definition stoch_procs where
  "stoch_procs M N = {X. ∀t. (X t) ∈ measurable M N}"

subsubsection ‹Adapted stochastic processes›

definition adapt_stoch_proc where
  "(adapt_stoch_proc F X N) ⟷ (∀t. (X t) ∈ measurable (F t) N)"


abbreviation "borel_adapt_stoch_proc F X ≡ adapt_stoch_proc F X borel"

lemma (in filtrated_prob_space) adapted_is_dsp:
  assumes "adapt_stoch_proc F X N"
  shows "X ∈ stoch_procs M N"
  unfolding  stoch_procs_def
  by (intro CollectI, (meson adapt_stoch_proc_def assms filtration filtration_def measurable_from_subalg))


lemma (in filtrated_prob_space) adapt_stoch_proc_borel_measurable:
  assumes "adapt_stoch_proc F X N"
  shows "∀n. (X n) ∈ measurable M N"
proof
  fix n
  have "X n ∈ measurable (F n) N" using assms unfolding  adapt_stoch_proc_def by simp
  moreover have "subalgebra M (F n)" using filtration unfolding filtration_def by simp
  ultimately show "X n ∈ measurable M N" by (simp add:measurable_from_subalg)
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_borel_measurable:
  assumes "borel_adapt_stoch_proc F X"
  shows "∀n. (X n) ∈ borel_measurable M"
proof
  fix n
  have "X n ∈ borel_measurable (F n)" using assms unfolding  adapt_stoch_proc_def by simp
  moreover have "subalgebra M (F n)" using filtration unfolding filtration_def by simp
  ultimately show "X n ∈ borel_measurable M" by (simp add:measurable_from_subalg)
qed


lemma (in filtrated_prob_space) constant_process_borel_adapted:
  shows "borel_adapt_stoch_proc F (λ n w. c)"
unfolding  adapt_stoch_proc_def
proof
  fix t
  show "(λw. c) ∈ borel_measurable (F t)" using borel_measurable_const by blast
qed


lemma (in filtrated_prob_space) borel_adapt_stoch_proc_add:
  fixes X::"'b ⇒ 'a ⇒ ('c::{second_countable_topology, topological_monoid_add})"
  assumes "borel_adapt_stoch_proc F X"
  and "borel_adapt_stoch_proc F Y"
shows "borel_adapt_stoch_proc F (λt w. X t w + Y t w)" unfolding adapt_stoch_proc_def
proof
  fix t
  have "X t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  moreover have "Y t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  ultimately show "(λw. X t w + Y t w) ∈ borel_measurable (F t)" by simp
qed


lemma (in filtrated_prob_space) borel_adapt_stoch_proc_sum:
  fixes A::"'d ⇒ 'b ⇒ 'a ⇒ ('c::{second_countable_topology, topological_comm_monoid_add})"
  assumes "⋀i. i∈ S ⟹ borel_adapt_stoch_proc F (A i)"
shows "borel_adapt_stoch_proc F (λ t w. (∑ i∈ S. A i t w))" unfolding adapt_stoch_proc_def
proof
  fix t
  have "⋀i. i∈ S⟹ A i t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  thus "(λ w. (∑ i∈ S. A i t w)) ∈ borel_measurable (F t)" by (simp add:borel_measurable_sum)
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_times:
  fixes X::"'b ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_algebra})"
  assumes "borel_adapt_stoch_proc F X"
  and "borel_adapt_stoch_proc F Y"
shows "borel_adapt_stoch_proc F (λt w. X t w * Y t w)" unfolding adapt_stoch_proc_def
proof
  fix t
  have "X t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  moreover have "Y t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  ultimately show "(λw. X t w * Y t w) ∈ borel_measurable (F t)" by simp
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_prod:
  fixes A::"'d ⇒ 'b ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_field})"
  assumes "⋀i. i∈ S ⟹ borel_adapt_stoch_proc F (A i)"
shows "borel_adapt_stoch_proc F (λ t w. (∏ i∈ S. A i t w))" unfolding adapt_stoch_proc_def
proof
  fix t
  have "⋀i. i∈ S⟹ A i t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  thus "(λ w. (∏ i∈ S. A i t w)) ∈ borel_measurable (F t)" by simp
qed


subsubsection ‹Predictable stochastic processes›

definition predict_stoch_proc where
  "(predict_stoch_proc F X N) ⟷ (X 0 ∈ measurable (F 0) N ∧ (∀n. (X (Suc n)) ∈ measurable (F n) N))"


abbreviation  "borel_predict_stoch_proc F X ≡ predict_stoch_proc F X borel"

lemma (in disc_filtr_prob_space) predict_imp_adapt:
  assumes "predict_stoch_proc F X N"
  shows "adapt_stoch_proc F X N" unfolding adapt_stoch_proc_def
proof
  fix n
  show "X n ∈ measurable (F n) N"
  proof (cases "n = 0")
    case True
    thus ?thesis using assms unfolding predict_stoch_proc_def by auto
  next
    case False
    thus ?thesis using assms unfolding predict_stoch_proc_def
      by (metis Suc_n_not_le_n increasing_measurable_info nat_le_linear not0_implies_Suc)
  qed
qed


lemma (in disc_filtr_prob_space) predictable_is_dsp:
  assumes "predict_stoch_proc F X N"
  shows "X ∈ stoch_procs M N"
unfolding  stoch_procs_def
proof
  show "∀n. random_variable N (X n)"
  proof
    fix n
    show "random_variable N (X n)"
    proof (cases "n=0")
      case True
      thus ?thesis using assms unfolding predict_stoch_proc_def
        using filtration filtration_def measurable_from_subalg by blast
    next
      case False
      thus ?thesis using assms unfolding predict_stoch_proc_def
        by (metis filtration filtration_def measurable_from_subalg not0_implies_Suc)
    qed
  qed
qed



lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_borel_measurable:
  assumes "borel_predict_stoch_proc F X"
  shows "∀n. (X n) ∈ borel_measurable M" using assms predictable_is_dsp unfolding stoch_procs_def by auto



lemma (in disc_filtr_prob_space) constant_process_borel_predictable:
  shows "borel_predict_stoch_proc F (λ n w. c)"
unfolding  predict_stoch_proc_def
proof
  show "(λw. c) ∈ borel_measurable (F 0)" using borel_measurable_const by blast
next
  show "∀n. (λw. c) ∈ borel_measurable (F n)" using borel_measurable_const by blast
qed

lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_add:
  fixes X::"nat ⇒ 'a ⇒ ('c::{second_countable_topology, topological_monoid_add})"
  assumes "borel_predict_stoch_proc F X"
  and "borel_predict_stoch_proc F Y"
shows "borel_predict_stoch_proc F (λt w. X t w + Y t w)" unfolding predict_stoch_proc_def
proof
  show "(λw. X 0 w + Y 0 w) ∈ borel_measurable (F 0)"
    using assms(1) assms(2) borel_measurable_add predict_stoch_proc_def by blast
next
  show "∀n. (λw. X (Suc n) w + Y (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "X (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X (Suc n) w + Y (Suc n) w) ∈ borel_measurable (F n)" by simp
  qed
qed



lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_sum:
  fixes A::"'d ⇒ nat ⇒ 'a ⇒ ('c::{second_countable_topology, topological_comm_monoid_add})"
  assumes "⋀i. i∈ S ⟹ borel_predict_stoch_proc F (A i)"
shows "borel_predict_stoch_proc F (λ t w. (∑ i∈ S. A i t w))" unfolding predict_stoch_proc_def
proof
  show "(λw. ∑i∈S. A i 0 w) ∈ borel_measurable (F 0)"
  proof
    have "⋀i. i∈ S⟹ A i 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∑ i∈ S. A i 0 w)) ∈ borel_measurable (F 0)" by (simp add:borel_measurable_sum)
  qed simp
next
  show "∀n. (λw. ∑i∈S. A i (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "⋀i. i∈ S⟹ A i (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∑ i∈ S. A i (Suc n) w)) ∈ borel_measurable (F n)" by (simp add:borel_measurable_sum)
  qed
qed


lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_times:
  fixes X::"nat ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_algebra})"
  assumes "borel_predict_stoch_proc F X"
  and "borel_predict_stoch_proc F Y"
shows "borel_predict_stoch_proc F (λt w. X t w * Y t w)" unfolding predict_stoch_proc_def
proof
  show "(λw. X 0 w * Y 0 w) ∈ borel_measurable (F 0)"
  proof -
    have "X 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X 0 w * Y 0 w) ∈ borel_measurable (F 0)" by simp
  qed
next
  show "∀n. (λw. X (Suc n) w * Y (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "X (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X (Suc n) w * Y (Suc n) w) ∈ borel_measurable (F n)" by simp
  qed
qed

lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_prod:
  fixes A::"'d ⇒ nat ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_field})"
  assumes "⋀i. i∈ S ⟹ borel_predict_stoch_proc F (A i)"
shows "borel_predict_stoch_proc F (λ t w. (∏ i∈ S. A i t w))" unfolding predict_stoch_proc_def
proof
  show "(λw. ∏i∈S. A i 0 w) ∈ borel_measurable (F 0)"
  proof -
    have "⋀i. i∈ S⟹ A i 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∏ i∈ S. A i 0 w)) ∈ borel_measurable (F 0)" by simp
  qed
next
  show "∀n. (λw. ∏i∈S. A i (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "⋀i. i∈ S⟹ A i (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∏ i∈ S. A i (Suc n) w)) ∈ borel_measurable (F n)" by simp
  qed
qed


definition (in prob_space) constant_image where
  "constant_image f = (if ∃ c::'b::{t2_space}. ∀x∈ space M. f x = c then
    SOME c. ∀x ∈ space M. f x = c else undefined)"

lemma (in prob_space) constant_imageI:
  assumes "∃c::'b::{t2_space}. ∀x∈ space M. f x = c"
  shows "∀x∈ space M. f x = (constant_image f)"
proof
  fix x
  assume "x∈ space M"
  let ?c = "SOME c. ∀x∈ space M. f x = c"
  have "f x = ?c" using ‹x∈ space M› someI_ex[of "λc. ∀x∈ space M. f x = c"] assms by blast
  thus "f x = (constant_image f)" by (simp add: assms prob_space.constant_image_def prob_space_axioms)
qed

lemma (in prob_space) constant_image_pos:
  assumes "∀x∈ space M. (0::real) < f x"
  and "∃c::real. ∀x∈ space M. f x = c"
shows "0 < (constant_image f)"
proof -
  {
    fix x
    assume "x∈ space M"
    hence "0 < f x" using assms by simp
    also have "... = constant_image f" using assms constant_imageI ‹x∈ space M› by auto
    finally have ?thesis .
  }
  thus ?thesis using subprob_not_empty by auto
qed

definition open_except where
"open_except x y = (if x = y then {} else SOME A. open A ∧ x∈ A ∧ y∉ A)"


lemma open_exceptI:
  assumes "(x::'b::{t1_space}) ≠ y"
  shows "open (open_except x y)" and "x∈ open_except x y" and  "y∉ open_except x y"
proof-
  have ex:"∃U. open U ∧ x ∈ U ∧ y ∉ U" using ‹x≠ y› by (simp add:t1_space)
  let ?V = "SOME A. open A ∧ x∈ A ∧ y∉ A"
  have vprop: "open ?V ∧ x ∈ ?V ∧ y ∉ ?V" using someI_ex[of "λU. open U ∧ x ∈ U ∧ y ∉ U"] ex by blast
  show "open (open_except x y)" by (simp add: open_except_def vprop)
  show "x∈ open_except x y" by (metis (full_types) open_except_def vprop)
  show "y∉ open_except x y" by (metis (full_types) open_except_def vprop)
qed

lemma open_except_set:
  assumes "finite A"
  and "(x::'b::{t1_space}) ∉ A"
shows "∃U. open U ∧ x∈ U ∧ U∩ A = {}"
proof(intro exI conjI)
  have "∀y∈ A. x≠ y" using assms by auto
  let ?U = "⋂ y ∈ A. open_except x y"
  show "open ?U"
  proof (intro open_INT ballI, (simp add: assms))
    fix y
    assume "y∈ A"
    show "open (open_except x y)" using ‹∀y∈ A. x≠ y› by (simp add: ‹y ∈ A› open_exceptI)
  qed
  show "x ∈ (⋂y∈A. open_except x y)"
  proof
    fix y
    assume "y∈ A"
    show "x∈open_except x y" using ‹∀y∈ A. x≠ y› by (simp add: ‹y ∈ A› open_exceptI)
  qed
  have "∀y∈A. y∉ ?U" using ‹∀y∈ A. x≠ y› open_exceptI(3) by auto
  thus "(⋂y∈A. open_except x y) ∩ A = {}" by auto
qed

definition open_exclude_set where
"open_exclude_set x A = (if (∃U. open U ∧ U∩ A = {x}) then SOME U. open U ∧ U ∩ A = {x} else {})"

lemma open_exclude_setI:
  assumes "∃U. open U ∧ U∩ A = {x}"
shows "open (open_exclude_set x A)" and "(open_exclude_set x A) ∩ A = {x}"
proof -
  let ?V = "SOME U. open U ∧ U ∩ A = {x}"
  have vprop: "open ?V ∧ ?V ∩ A = {x}" using someI_ex[of "λU. open U ∧ U ∩ A = {x}"] assms by blast
  show "open (open_exclude_set x A)" by (simp add: open_exclude_set_def vprop)
  show "open_exclude_set x A ∩ A = {x}" by (metis (mono_tags, lifting) open_exclude_set_def vprop)
qed

lemma open_exclude_finite:
  assumes "finite A"
  and "(x::'b::{t1_space})∈ A"
shows open_set: "open (open_exclude_set x A)" and inter_x:"(open_exclude_set x A) ∩ A = {x}"
proof -
  have "∃U. open U ∧ U∩ A = {x}"
  proof -
    have "∃U. open U ∧ x∈ U ∧ U∩ (A-{x}) = {}"
    proof (rule open_except_set)
      show "finite (A -{x})" using assms by auto
      show "x∉ A -{x}" by simp
    qed
    thus ?thesis using assms by auto
  qed
  thus "open (open_exclude_set x A)" and "(open_exclude_set x A) ∩ A = {x}" by (auto simp add: open_exclude_setI)
qed

subsection ‹Initially trivial filtrations›
text ‹Intuitively, these are filtrations that can be used to denote the fact that there is no information at the start.›

definition init_triv_filt::"'a measure ⇒ ('i::linorder_bot ⇒ 'a measure) ⇒ bool" where
  "init_triv_filt M F ⟷ filtration M F ∧ sets (F bot) = {{}, space M}"

lemma triv_measurable_cst:
  fixes f::"'a⇒'b::{t2_space}"
  assumes "space N = space M"
  and "space M ≠ {}"
  and "sets N = {{}, space M}"
  and "f∈ measurable N borel"
shows "∃ c::'b. ∀x∈ space N. f x = c"
proof -
  have "f `(space N) ≠ {}" using assms by (simp add: assms)
  hence "∃ c. c∈ f`(space N)" by auto
  from this obtain c where "c∈ f`(space N)" by auto
  have "∀x ∈ space N. f x = c"
  proof
    fix x
    assume "x∈ space N"
    show "f x = c"
    proof (rule ccontr)
      assume "f x ≠ c"
      hence "(∃U V. open U ∧ open V ∧ (f x) ∈ U ∧ c ∈ V ∧ U ∩ V = {})" by (simp add: separation_t2)
      from this obtain U and V where "open U" and "open V" and "(f x) ∈ U" and "c ∈ V" and "U ∩ V = {}" by blast
      have "(f -`V) ∩ space N = space N"
      proof -
        have "V∈ sets borel" using ‹open V› unfolding borel_def by simp
        hence "(f -`V) ∩ space N ∈ sets N" using assms unfolding measurable_def by simp
        show "(f -`V) ∩ space N = space N"
        proof (rule ccontr)
          assume "(f -`V) ∩ space N ≠ space N"
          hence "(f -`V) ∩ space N = {}" using assms ‹(f -`V) ∩ space N ∈ sets N› by simp
          thus False using ‹c∈V› using ‹c ∈ f ` space N› by blast
        qed
      qed
      have "((f-`U)∩ space N) ∩ ((f-`V) ∩ space N) = {}" using ‹U∩V = {}› by auto
      moreover have "(f -`U) ∩ space N ∈ sets N" using assms ‹open U› unfolding measurable_def by simp
      ultimately have "(f -`U) ∩ space N = {}" using assms ‹(f -`V) ∩ space N = space N› by simp
      thus False using ‹f x ∈ U› ‹x ∈ space N› by blast
    qed
  qed
  thus "∃ c. ∀x∈ space N. f x = c" by auto
qed

locale trivial_init_filtrated_prob_space = prob_space +
  fixes F
  assumes info_filtration: "init_triv_filt M F"

sublocale trivial_init_filtrated_prob_space ⊆ filtrated_prob_space
  using info_filtration unfolding init_triv_filt_def by (unfold_locales, simp)


locale triv_init_disc_filtr_prob_space = prob_space +
  fixes F
  assumes info_disc_filtr: "disc_filtr M F ∧ sets (F bot) = {{}, space M}"

sublocale triv_init_disc_filtr_prob_space ⊆ trivial_init_filtrated_prob_space
proof unfold_locales
  show "init_triv_filt M F" using info_disc_filtr bot_nat_def unfolding init_triv_filt_def disc_filtr_def
    by (simp add: filtrationI)

qed


sublocale triv_init_disc_filtr_prob_space ⊆ disc_filtr_prob_space
proof unfold_locales
  show "disc_filtr M F" using info_disc_filtr by simp
qed

lemma (in triv_init_disc_filtr_prob_space) adapted_init:
  assumes "borel_adapt_stoch_proc F x"
  shows "∃c. ∀w ∈ space M. ((x 0 w)::real) = c"
proof -
  have "space M = space (F 0)" using filtration
    by (simp add: filtration_def subalgebra_def)
  moreover have "∃c. ∀w ∈ space (F 0). x 0 w = c"
  proof (rule triv_measurable_cst)
    show "space (F 0) = space M" using ‹space M = space (F 0)› ..
    show "sets (F 0) = {{}, space M}" using info_disc_filtr
      by (simp add: init_triv_filt_def bot_nat_def)
    show "x 0 ∈ borel_measurable (F 0)" using assms by (simp add: adapt_stoch_proc_def)
    show "space M ≠ {}" by (simp add:not_empty)
  qed
  ultimately show ?thesis by simp
qed

subsection ‹Filtration-equivalent measure spaces›
text ‹This is a relaxation of the notion of equivalent probability spaces, where equivalence is tested modulo a
filtration. Equivalent measure spaces agree on events that have a zero probability of occurring; here, filtration-equivalent
measure spaces agree on such events when they belong to the filtration under consideration.›

definition filt_equiv where
"filt_equiv F M N ⟷ sets M = sets N ∧ filtration M F  ∧ (∀ t A. A ∈ sets (F t) ⟶ (emeasure M A = 0) ⟷ (emeasure N A = 0))"


lemma filt_equiv_space:
  assumes "filt_equiv F M N"
  shows "space M = space N" using assms unfolding filt_equiv_def
 filtration_def subalgebra_def by (meson sets_eq_imp_space_eq)

lemma filt_equiv_sets:
  assumes "filt_equiv F M N"
  shows "sets M = sets N" using assms unfolding filt_equiv_def by simp



lemma filt_equiv_filtration:
  assumes "filt_equiv F M N"
  shows "filtration N F" using assms unfolding filt_equiv_def filtration_def subalgebra_def
  by (metis sets_eq_imp_space_eq)




lemma (in filtrated_prob_space) AE_borel_eq:
fixes f::"'a⇒real"
assumes "f∈ borel_measurable (F t)"
and "g∈ borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "{w∈ space M. f w ≠ g w} ∈ sets (F t) ∧ emeasure M {w∈ space M. f w ≠ g w} = 0"
proof
  show "{w ∈ space M. f w ≠ g w} ∈ sets (F t)"
  proof -
    define minus where "minus = (λw. (f w) - (g w))"
    have "minus ∈ borel_measurable (F t)" unfolding minus_def using assms by simp
    hence "{w∈ space (F t). 0 < minus w} ∈ sets (F t)" using borel_measurable_iff_greater by auto
    moreover have "{w∈ space (F t). minus w < 0} ∈ sets (F t)" using borel_measurable_iff_less
      ‹minus ∈ borel_measurable (F t)› by auto
    ultimately have "{w∈ space (F t). 0 < minus w} ∪ {w∈ space (F t). minus w < 0} ∈ sets (F t)" by simp
    moreover have "{w∈ space (F t). f w ≠ g w} = {w∈ space (F t). 0 < minus w} ∪ {w∈ space (F t). minus w < 0}"
    proof
      show "{w ∈ space (F t). f w ≠ g w} ⊆ {w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0}"
      proof
        fix w
        assume "w ∈ {w ∈ space (F t). f w ≠ g w}"
        hence "w∈ space (F t)" and "f w ≠ g w" by auto
        thus "w∈ {w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0}" unfolding minus_def
          by (cases "f w < g w") auto
      qed
      have "{w ∈ space (F t). 0 < minus w} ⊆ {w ∈ space (F t). f w ≠ g w}" unfolding minus_def by auto
      moreover have "{w ∈ space (F t). minus w < 0} ⊆ {w ∈ space (F t). f w ≠ g w}" unfolding minus_def by auto
      ultimately show "{w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0} ⊆ {w ∈ space (F t). f w ≠ g w}"
        by simp
    qed
    moreover have "space (F t) = space M" using filtration unfolding filtration_def subalgebra_def by simp
    ultimately show ?thesis by simp
  qed
  show "emeasure M {w∈ space M. f w ≠ g w} = 0" by (metis (no_types) AE_iff_measurable assms(3) emeasure_notin_sets)
qed


lemma (in prob_space) filt_equiv_borel_AE_eq:
  fixes f::"'a⇒ real"
  assumes "filt_equiv F M N"
and "f∈ borel_measurable (F t)"
and "g∈ borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "AE w in N. f w = g w"
proof -
  have set0: "{w∈ space M. f w ≠ g w} ∈ sets (F t) ∧ emeasure M {w∈ space M. f w ≠ g w} = 0"
  proof (rule filtrated_prob_space.AE_borel_eq, (auto simp add: assms))
    show "filtrated_prob_space M F" using assms unfolding filt_equiv_def
      by (simp add: filtrated_prob_space_axioms.intro filtrated_prob_space_def prob_space_axioms)
  qed
  hence "emeasure N {w∈ space M. f w ≠ g w} = 0" using assms unfolding filt_equiv_def by auto
  moreover have "{w∈ space M. f w ≠ g w} ∈ sets N" using set0 assms unfolding filt_equiv_def
    filtration_def subalgebra_def by auto
  ultimately show ?thesis
  proof -
  have "space M = space N"
    by (metis assms(1) filt_equiv_space)
    then have "∀p. almost_everywhere N p ∨ {a ∈ space N. ¬ p a} ≠ {a ∈ space N. f a ≠ g a}"
      using AE_iff_measurable ‹emeasure N {w ∈ space M. f w ≠ g w} = 0› ‹{w ∈ space M. f w ≠ g w} ∈ sets N›
      by auto
    then show ?thesis
      by metis
  qed
qed

lemma filt_equiv_prob_space_subalgebra:
  assumes "prob_space N"
  and "filt_equiv F M N"
  and "sigma_finite_subalgebra M G"
shows "sigma_finite_subalgebra N G" unfolding sigma_finite_subalgebra_def
proof
  show "subalgebra N G"
    by (metis assms(2) assms(3) filt_equiv_space filt_equiv_def sigma_finite_subalgebra_def subalgebra_def)
  show "sigma_finite_measure (restr_to_subalg N G)" unfolding restr_to_subalg_def
    by (metis ‹subalgebra N G› assms(1) finite_measure_def finite_measure_restr_to_subalg prob_space_def restr_to_subalg_def)
qed


lemma filt_equiv_measurable:
  assumes "filt_equiv F M N"
  and "f∈ measurable M P"
shows "f∈ measurable N P" using assms unfolding filt_equiv_def measurable_def
proof -
  assume a1: "sets M = sets N ∧ Filtration.filtration M F ∧ (∀t A. A ∈ sets (F t) ⟶ (emeasure M A = 0) = (emeasure N A = 0))"
  assume a2: "f ∈ {f ∈ space M → space P. ∀y∈sets P. f -` y ∩ space M ∈ sets M}"
  have "space N = space M"
    using a1 by (metis (lifting) sets_eq_imp_space_eq)
  then show "f ∈ {f ∈ space N → space P. ∀C∈sets P. f -` C ∩ space N ∈ sets N}"
    using a2 a1 by force
qed


lemma filt_equiv_imp_subalgebra:
  assumes "filt_equiv F M N"
shows "subalgebra N M" unfolding subalgebra_def
  using assms filt_equiv_space filt_equiv_def by blast




end